\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{listings}
\usepackage{oz, amsfonts}
\usepackage{graphicx}

\title{Software Engineering\\Assignment 4}
\author{Adrian.Nembach@uni-konstanz.de 01/842319\\Udo.3.Schlegel@uni-konstanz.de 01/840835\\Sirui.Liu@uni-konstanz.de 01/857316}
\begin{document}
\maketitle

\section*{Exercise 4.1}
\begin{itemize}
\item Precondition: To ensure that the precondition is kept or weakened, we can join the precondition of B with the precondition of A with an $\lor$ operator\\
\begin{equation}
(x_1 < 50\ \&\ x_2 < 50) \lor (x_1 < 60\ \&\ x_2 < 60)
\end{equation}
The result is 
\begin{equation}
x_1 < 60 \ \&\ x_2 < 60
\end{equation}
Therefore the precondition of B is weaker than the precondition of A
\item Postcondition: To ensure that the postcondition is kept or strengthened, we can join the postcondition of B with the postcondition of A with an $\land$ operator\\
\begin{equation}
(calculateSUM(x_1,x_2)<100) \land (calculateSUM(x_1,x_2)<80)
\end{equation}
The result is 
\begin{equation}
calculateSUM(x_1,x_2)<80
\end{equation}
Therefore the postcondition of B is stronger than the postcondition of A
\item The principle of subcontracting is met, so it is legal.
\end{itemize}
\newpage
\section*{Exercise 4.2}

\begin{center}
\includegraphics[scale=0.60]{HSM2b.png}
\end{center}


\section*{Exercise 4.3}
For the following diagram we assumed that in order for the caller to be able to call the callee there are the following entities needed:
\begin{itemize}
\item caller\_phone
\item caller\_line
\item callee\_line
\item callee\_phone
\end{itemize}
(We made these assumptions based on the given exercise text)
\begin{center}
\includegraphics[scale=0.45]{SQD3a.png}
\end{center}


\end{document}